A:Type, eq:EqDecider(A), B:(AType), f,g,h:fpf(A; a.B(a)).
fpf-compatible(A; a.B(a); eq; f; g)
 (fpf-compatible(A; a.B(a); eq; h; fpf-join(eq; f; g))
  (fpf-compatible(A; a.B(a); eq; h; f)  fpf-compatible(A; a.B(a); eq; h; g))) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), x(s), x. t(x), fpf(A; a.B(a)), fpf-compatible(A; a.B(a); eq; f; g), prop{i:l}, P  Q, fpf-join(eq; f; g), P  Q, P  Q, P  Q, fpf-ap(f; eq; x), b, top, fpf-dom(eq; x; f), P  Q, False, A, b, , guard(T), sq_type(T)
Lemmas	fpf-compatible-join, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, fpf-join-ap, fpf-join-dom, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-join wf, fpf-compatible wf, fpf wf, deq wf